def h : BV 32 → Array Bool :=
fun x => (fun x => g (f x).val) x
def r : Nat → Prop :=
fun a => if (a == 0) = true then (a != 1) = true else (a != 2) = true
def r : (a : Nat) → Prop :=
fun (a : Nat) =>
  @ite.{1} Prop
    (@Eq.{1} Bool
      (@BEq.beq.{0} Nat (@instBEqOfDecidableEq.{0} Nat instDecidableEqNat) a
        (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))
      Bool.true)
    (instDecidableEqBool
      (@BEq.beq.{0} Nat (@instBEqOfDecidableEq.{0} Nat instDecidableEqNat) a
        (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))
      Bool.true)
    (@Eq.{1} Bool
      (@bne.{0} Nat (@instBEqOfDecidableEq.{0} Nat instDecidableEqNat) a
        (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
      Bool.true)
    (@Eq.{1} Bool
      (@bne.{0} Nat (@instBEqOfDecidableEq.{0} Nat instDecidableEqNat) a
        (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
      Bool.true)
def s : Option Nat :=
myFun.f 3 <|> myFun.f 4