1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
eqT_rect@{u u0} =
fun (A : Type@{u}) (a : A) (P : forall a0 : A, eqT@{u} a a0 -> Type@{u0})
(f : P a (reflT@{u} a)) (a0 : A) (e : eqT@{u} a a0) =>
match e :> eqT@{u} a _ as e0 in (eqT _ a1) return (P a1 e0) with
| reflT _ => f
end
: forall (A : Type@{u}) (a : A)
(P : forall a0 : A, eqT@{u} a a0 -> Type@{u0}),
P a (reflT@{u} a) -> forall (a0 : A) (e : eqT@{u} a a0), P a0 e
(* u u0 |= *)
Arguments eqT_rect A%type_scope a P%function_scope f a0 e
seq_rect =
fun (A : Type@{seq.u0}) (a : A)
(P : forall a0 : A, seq a a0 -> Type@{PrintMatch.10})
(f : P a (srefl a)) (a0 : A) (s : seq a a0) =>
match s :> seq a a0 as s0 in (seq _ a1) return (P a1 s0) with
| srefl _ => f
end
: forall (A : Type@{seq.u0}) (a : A)
(P : forall a0 : A, seq a a0 -> Type@{PrintMatch.10}),
P a (srefl a) -> forall (a0 : A) (s : seq a a0), P a0 s
Arguments seq_rect A%type_scope a P%function_scope f a0 s
eq_sym =
fun (A : Type) (x y : A) (H : @eq A x y) =>
match H in (@eq _ _ a) return (@eq A a x) with
| @eq_refl _ _ => @eq_refl A x
end
: forall [A : Type] [x y : A] (_ : @eq A x y), @eq A y x
Arguments eq_sym [A]%type_scope [x y] _
eq_sym =
fun (A : Type) (x y : A) (H : x = y) =>
match H in (_ = a) return (a = x) with
| @eq_refl _ _ => @eq_refl A x
end
: forall [A : Type] [x y : A], x = y -> y = x
Arguments eq_sym [A]%type_scope [x y] _
eq_sym =
fun (A : Type) (x y : A) (H : x = y) =>
match H in (_ = a) return (a = x) with
| @eq_refl _ _ => @eq_refl A x
end
: forall [A : Type] [x y : A], x = y -> y = x
Arguments eq_sym [A]%type_scope [x y] _
|
