include "ground_2/xoa/xoa.ma".
-(* Properties with multiple existental quantifier (5, 1) ********************)
+(* Properties with multiple existental quantifier (4, 1) ********************)
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.