AbsPatternMatch/Basic.v at master · disteph/AbsPatternMatch · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Require Import Coq.Program.Equality.
Generalizable All Variables.

Notation "{{ p , v }}" := (existS _ p v).

Lemma elim2: forall (U : Type) (P : U -> Type) (p : U) (x y : P p),
               {{p, x}} = {{p, y}} -> x = y.
Proof.
  exact inj_pair2.
Qed.
Arguments elim2 {U P p x y} _.

Record SClass {A:Type} (h:A) :=
  { IClass := A;
    get : A := h}.

Arguments IClass {A h} _.
Arguments get {A h} _.