|
Require Import TestSuite.admit.
Require Setoid.
Variables P Q : forall {T : Set}, T -> Prop.
Lemma rule{T : Set}{x : T} : Q x <-> P x. admit. Qed.
Goal forall (T : Set)(x : T), Q x <-> P x.
Proof.
intros T x.
setoid_rewrite rule.
reflexivity.
Qed.
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
