Inductive P : A -> Type := c1 : forall a, P a | c2 : forall a, P a. (* requires at least two constructors for the issue to appear *)
#[local] Instance P_R : Proper (R ==> arrow) P. Admitted.
Goalforall a b, R a b -> P a -> P b. Proof. intros a b HR HP.
Succeed rewrite HR in HP.
Succeed rewrite <- HR. apply (P_R _ _ HR HP). Qed.
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.
