Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/dep_pair_eq.v

Created November 3, 2019 11:05
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 Blaisorblade/b62db42705a91661516592c753cdb228 to your computer and use it in GitHub Desktop.
Save Blaisorblade/b62db42705a91661516592c753cdb228 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
dep_pair_eq.v
Require Import ProofIrrelevance.
Section dep_pair.
Context {A : Type} {P : A -> Prop}.
Definition dep_pair := ex_intro P.
Lemma dep_pair_eq (a1 a2 : A) p1 p2: a1 = a2 -> dep_pair a1 p1 = dep_pair a2 p2.
Proof.
intros ->.
(* Now f_equal can reduce the equality to a homogeneous one, so it works. *)
f_equal.
apply proof_irrelevance.
Qed.
End dep_pair.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment