|
Require Import Setoid.
Parameter F : nat -> nat.
Axiom F_id : forall n : nat, n = F n.
Goal forall n : nat, F n = n.
intro n. setoid_rewrite F_id at 3. reflexivity.
Qed.
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
