compose 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 x]%_nat_scope h
map id (1 :: nil)
: list nat
map id' (1 :: nil)
: list nat
map (id'' (A:=nat)) (1 :: nil)
: list nat
fix f (x : nat) : option nat := match x with
| 0 => None
| S _ => x
end
: nat -> option nat
fun x : False => let y := False_rect (A:=bool) x in y
: False -> bool
fun x : False => let y : True := False_rect x in y
: False -> True
[ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
]
