proposition: Lemma demo_lets : (H1 -> H2 -> H3 /\ H4) -> (H1 -> H2) -> H1 -> H3.
proof: Proof. Proof using. intros P Q R. lets U: (Q R). lets [V W]: (P R U). lets V1 W1: (P R U). lets: (P R). lets U': U. demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia