proposition: Lemma goal_model_example (ci : Ti) (dj : Tj := ej) (Fk : Pk ci) : forall (xl : Tl), let ym := bm in Pn xl -> Conclusion ci dj ym xl.
proof: Proof. Abort. Lemma goal_model_example (ci : Ti) (dj : Tj := ej) (Fk : Pk ci) : forall (xl : Tl), let ym := bm in Pn xl -> Conclusion ci dj ym xl. Proof. move=> xl ym pnxl. move: ci Fk. Abort. Lemma goal_model_example (ci : Ti) (dj : Tj := ej) (Fk : Pk ci) : forall (xl : Tl), let ym := bm in Pn xl -> Conclusion ci dj ym xl. Proof. move=> xl /= pnxl. Fail move=> {xl}. Fail move=> {dj}. rewrite /dj {dj}. move: ci Fk. move=> {pnxl}. move=> ci _. Abort. Lemma addnA m n p : m + (n + p) = (m + n) + p. Proof. by elim: m => // m IHm; rewrite !addSn IHm. Restart. Proof. by elim: m => // m; rewrite !addSn => ->. Qed.
imports: mathcomp(all_ssreflect)