|
(* Checking that the "in" clause takes the "eqn" clause into account *)
Definition test (x: nat): {y: nat | False }. Admitted.
Parameter x: nat.
Parameter z: nat.
Goal
proj1_sig (test x) = z ->
False.
Proof.
intro H.
destruct (test x) eqn:Heqs in H.
change (test x = exist (fun _ : nat => False) x0 f) in Heqs. (* Check it has the expected statement *)
Abort.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.31Angebot
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
|
