(* USARE L'ESISTENZIALE DEBOLE *)
definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
-notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation > "'If' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation < "'If' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
notation > "hvbox(a break ≤ b)" non associative with precedence 45 for @{oa_leq $a $b}.
oa_zero_bot: ∀p:oa_P.𝟘 ≤ p;
oa_one_top: ∀p:oa_P.p ≤ 𝟙;
oa_overlap_preserves_meet_: ∀p,q:oa_P.p >< q →
- p >< (⋀ { x ∈ BOOL | if x then p else q(*match x with [ true ⇒ p | false ⇒ q ]*) | IF_THEN_ELSE_p oa_P p q });
+ p >< (⋀ { x ∈ BOOL | If x then p else q(*match x with [ true ⇒ p | false ⇒ q ]*) | IF_THEN_ELSE_p oa_P p q });
oa_join_split: ∀I:SET.∀p.∀q:I ⇒_2 oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));
(*oa_base : setoid;
1) enum non e' il nome giusto perche' non e' suriettiva