Haftungsausschluß.v KontaktUnknown {[0] [0] [0]}diese Dinge liegen außhalb unserer Verantwortung
Axiom X : Type.
Goal forall (x y z : X), X.
intro. Check x.
Set Mangle Names.
intro. Fail Check y. Check _0.
Set Mangle Names Light.
intro. Fail Check z. Fail Check _1. Check _z.
Abort.
Fixpoint Lots (n : nat) : Type :=
match n with
| 0 => X
| S k => forall (x : X), Lots k
end.
Goal Lots 10.
assert (_x8 : X) by admit.
cbv; intros.
Check _x9.
Abort.
Fixpoint Lots' (x : X) (n : nat) : Type :=
match n with
| 0 => X
| S k => forall _x, Lots' _x k
end.
Goal forall _x0, Lots' _x0 10.
assert (_x8 : X) by admit.
cbv; intros.
Check __x9.
simpl.
Abort.
[ Seitenstruktur0.99Drucken
]
