(* *)
(**************************************************************************)
+(* LOGIC ********************************************************************)
+
include "ground/xoa/ex_4_1.ma".
-(* Properties with multiple existental quantifier (4, 1) ********************)
+(* Constructions with ex4 ***************************************************)
lemma ex4_commute (A0) (P0,P1,P2,P3:A0→Prop):
(∃∃x0. P0 x0 & P1 x0 & P2 x0 & P3 x0) → ∃∃x0. P2 x0 & P3 x0 & P0 x0 & P1 x0.