+| 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;]