proposition: Lemma demo_sets_let_and_sets_eq_let : forall n1 n2 : nat, (let x := n1 + n2 in x = x) -> (let y := n2 + n1 in let z := y + y in z = z) -> (let t := n1 + n1 in t = t).
proof: Proof. Proof using. intros n1 n2 M1 M2. dup 3. sets_let a. sets_let b. sets_let c. auto. sets_let a in M1. auto. sets_eq_let a. sets_eq_let b. sets_eq_let c. auto. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia