proposition: Lemma AunionAx s u : Ain u (Aunion s) <-> exists t, Ain t s /\ Ain u t.
proof: Proof. split; intros H; destruct s as [A f]. - destruct H as [[a b] H]. exists (f a). split. + now exists a. + destruct (f a) as [C h]; simpl in *. now exists b. - destruct H as [[B g][[a Z1][b Z2]]]. apply Aeq_ASubq in Z1. specialize (Z1 (g b) (Ain_Asup g b)). apply Ain_pi in Z1 as [c H]. exists (existT _ a c). eauto. Qed.
imports: Setoid Morphisms