proposition: Lemma demo_sets_and_set_eq_and_sets_eq : forall n, ind (3 + n) -> ind (7 + n) -> ind (7 + n).
proof: Proof. Proof using. introv M1 M2. dup 9. sets a: (3+n). demo. sets b: (7+n). demo. set_eq a Ha: (7+n). demo. sets_eq a Ha: (7+n). demo. sets_eq a: (7+n). demo. sets_eq: (7+n). demo. set_eq a: (7+n) in M2. demo. set_eq a: (7+n) in |-. demo. sets_eq <- a: (7+n). demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia