+ (fun12 __ (oa_meet __) (mk_unary_morphism _ _ f _)).
+
+definition hint3: OAlgebra → setoid1.
+ intro; apply (oa_P o);
+qed.
+coercion hint3.
+
+definition hint4: ∀A. setoid2_OF_OAlgebra A → hint3 A.
+ intros; apply t;
+qed.
+coercion hint4.
+
+definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
+intros; split;
+[ intros (p q);
+ apply (∧ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
+| intros; lapply (prop12 ? O (oa_meet O BOOL));
+ [2: apply ({ x ∈ BOOL | match x with [ true ⇒ a | false ⇒ b ] | IF_THEN_ELSE_p ? a b });
+ |3: apply ({ x ∈ BOOL | match x with [ true ⇒ a' | false ⇒ b' ] | IF_THEN_ELSE_p ? a' b' });
+ | apply Hletin;]
+ intro x; simplify; cases x; simplify; assumption;]
+qed.
+
+notation "hovbox(a ∧ b)" left associative with precedence 35
+for @{ 'oa_meet_bin $a $b }.
+interpretation "o-algebra binary meet" 'oa_meet_bin a b =
+ (fun21 ___ (binary_meet _) a b).
+
+coercion Type1_OF_OAlgebra nocomposites.
+
+lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q).
+(* next change to avoid universe inconsistency *)
+change in ⊢ (?→%→%→?) with (Type1_OF_OAlgebra O);
+intros; lapply (oa_overlap_preserves_meet_ O p q f);
+lapply (prop21 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?);
+[3: apply (if ?? (Hletin1)); apply Hletin;|skip] apply refl1;
+qed.