Skip to content

Instantly share code, notes, and snippets.

@lthms

lthms/simpl_exist_eq.v

Created November 9, 2018 13:52
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save lthms/2aec9477e51f4c07e020a13aee4da3eb to your computer and use it in GitHub Desktop.
Save lthms/2aec9477e51f4c07e020a13aee4da3eb to your computer and use it in GitHub Desktop.
Download ZIP
Raw
simpl_exist_eq.v
Require Import Coq.Logic.ProofIrrelevance.
Require Import Coq.Program.Tactics.
Ltac simpl_exist_eq :=
match goal with
| [ |- exist _ ?x _ = exist _ ?y _]
=> let H := fresh "H"
in cut (x = y);
[ intro H;
apply eq_sig with (p:=H);
apply proof_irrelevance
| (* nothing *)
]
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment