[ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive l x);
apply (ap_rewr ??? (x∧x) (meet_refl l x)); assumption;
| intros 3 (x y z); unfold excl; intro H;
[ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive l x);
apply (ap_rewr ??? (x∧x) (meet_refl l x)); assumption;
| intros 3 (x y z); unfold excl; intro H;