proposition: Lemma demo_exist_1 : exists x1 x2 x3, x1 = x2 /\ x2 = x3 /\ x3 = 0.
proof: Proof. Proof using. dup 6. exists 0 0 0. auto. exists~ 0 0 0. exists __ 0 __. demo. exists 0 ___. exists. demo. Abort. Lemma demo_exists_2 : (exists n, n = 0) /\ (exists n m, n = m /\ n = 0) /\ (exists n, def_with_exists n) /\ (0 = 0). Proof using. splits. { exists. admit. } { exists. admit. } { exists. admit. } { try exists. admit. } Abort. Definition demo_let_binding_test_1 : ('let x := 3 in 'let y := x + x in y + y) = 12. Proof using. dup 3. reflexivity. simpl. let_simpl. let_simpl. reflexivity. let_name. let_name as z. subst x. subst z. reflexivity. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia