Parameter g : nat -> Prop. Axiom a : forall n, g (S n). Lemma foo (H : True) : exists n, g n /\ g n.
eexists.
clear H. split. simpleapply a. (* goal is "g (S ?Goal0@ {H:=H})" while H has long ceased to exist *) simpl. Abort.
¤ 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.0.11Bemerkung:
(vorverarbeitet)
¤
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.
