Inductive True : Prop := I. Class Lift (T : Type). Axiom closed_increment : forall {T} {H : Lift T}, True.
Create HintDb core. Lemma closed_monotonic T (H : Lift T) : True. Proof. Set Printing Universes.
eauto using closed_increment. Show Universes. Qed. (* also fails with -nois, so the content of the hint database does not matter
*)
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.
