(* bool-check-for-all problem example *)

let build_Vec := λ t: Type →
  let bv_intern := μ bv_intern →
    λ pvn: Nat → λ pv: Vec pvn t →
      λ n: Nat → match n {
        Z ⇒ pvn
        S n ⇒ λ x: t → bv_intern (S pvn) (Cons pv x) n
      };
  bv_intern Z Nil

let nat! := unary! Z S

let bcfamul :=
  μ bcfamul →
    λ n: Nat → λ f: (Vec n Bool → Bool) → match n {
      Z ⇒ f Nil;
      S n ⇒ bcfamul n (λ tv → do {
        f (Cons tv False);
        f (Cons tv True);
      })
    }

let n4 = nat! 4
bcfamul n4 (λ (build_Vec Bool n4 $a $b $c $d) : Vec n4 Bool → {
})