blob: d65d2a8f552033fbdbc2b57f9c51a9b68a7bbc60 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
compose (C:=nat) S
: (nat -> nat) -> nat -> nat
ex_intro (P:=fun _ : nat => True) (x:=0) I
: ex (fun _ : nat => True)
d2 = fun x : nat => d1 (y:=x)
: forall x x0 : nat, x0 = x -> x0 = x
Arguments d2 [x%nat_scope] [x0%nat_scope]
map id (1 :: nil)
: list nat
map id' (1 :: nil)
: list nat
map (id'' (A:=nat)) (1 :: nil)
: list nat
|
