blob: 46d8c26e83e4b642f97f1ca5babc0085a5637396 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Inductive foo (x := tt) := Foo : forall (y := x), foo.
Definition get (t : foo) := match t with Foo _ y => y end.
Goal get Foo = tt.
Proof.
reflexivity.
Qed.
Goal forall x : foo,
match x with Foo _ y => y end = match x with Foo _ _ => tt end.
Proof.
intros.
reflexivity.
Qed.
|
