eq_apply

alkabetz.v

Section alkabetz.
  Ltac eq_apply H :=
    match type of H with 
    | ?F ?X => 
      match goal with 
      | [  |- ?F ?Y ] => 
        replace Y with X; [exact H|]
      end
    end.
  
  Variable A : Type.
  Variable f : A -> Prop.
  Variable x y : A.
  Goal f x -> f y.
    intros.
    eq_apply H.
    (* now prove equality ... *) 
  Admitted.
End alkabetz.