proposition: Lemma demo_check_noevar_goal : forall (n:nat), (forall m, m = n -> True) -> True.
proof: Proof. Proof using. intros. check_noevar_goal. eapply H. try check_noevar_goal. dup. reflexivity. check_noevar_goal. auto. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia