proposition: Lemma forall_conj_inv_2 : forall (P Q : forall (x1:A1) (x2:A2 x1), Prop), (forall x1 x2, P x1 x2 /\ Q x1 x2) -> (forall x1 x2, P x1 x2) /\ (forall x1 x2, Q x1 x2).
proof: Proof. Proof using. prove_forall_conj_inv. Qed.
imports: TLC(LibTactics)