(* Check the behaviour of Simplify_eq *)
(* Check that Simplify_eq tries Intro until *)
Lemma l1 : 0 = 1 -> False.
simplify_eq 1.
Qed.
Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False.
simplify_eq H.
intros.
apply (n_Sn x H0).
Qed.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.2Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|