proposition: Lemma conj_strengthen_4 : forall (Q1 Q2 Q3 Q4 P1 P2 P3 P4 : Prop), (Q1 /\ Q2 /\ Q3 /\ Q4) -> (Q1 -> P1) -> (Q2 -> P2) -> (Q3 -> P3) -> (Q4 -> P4) -> (P1 /\ P2 /\ P3 /\ P4).
proof: Proof. Proof using. autos*. Qed.
imports: TLC(LibTactics)