type error with Prop?

Stream: lean4

[Alexandre Rademaker]

Maybe a stupid mistake... but

section

 variable (x e i h : Type)
 variable (_young_a_1 : e → x → Prop)
 variable (_boy_n_1 _kid_n_1 _smile_n_1 _man_n_1 : x → Prop)
 variable (place_n : x → Prop)
 variable (_outdoors_a_1 : e → x → Prop)
 variable (_play_v_1 : e → x → i → Prop)
 variable (loc_nonsp : e → e → x → Prop)
 variable (_smile_v_1 : e → x → i → Prop)
 variable (_nearby_p : e → e → Prop)
 variable (_and_c : e → e → e → Prop)
 variable (_with_p : e → x → x → Prop)
 variable (_near_p_state : e → e → x → Prop)

 def h₁ : Prop := ∃ i11 i25 e10 e26 e12 e3 e19 e9 e18,
  ∃ x7, (_young_a_1 e9 x7 ∧ _boy_n_1 x7) ∧
   (∃ x13, (place_n x13 ∧ _outdoors_a_1 e18 x13) ∧
    (∃ x23, _man_n_1 x23 ∧
            (_play_v_1 e10 x7 i11 ∧ loc_nonsp e12 e10 x13 ∧ _and_c e3 e10 e19 ∧ _smile_v_1 e19 x23 i25 ∧ _nearby_p e26 e19)))

 def h₂ : Prop := ∃ i9 e3 e23 e16 e10 e17,
  ∃ x7, _kid_n_1 x7 ∧
   (∃ x11, (place_n x11 ∧ _outdoors_a_1 e16 x11) ∧
    (∃ x18, (∃ x24, _smile_n_1 x24 ∧ _man_n_1 x18 ∧ _with_p e23 x18 x24) ∧ (_play_v_1 e3 x7 i9 ∧ loc_nonsp e10 e3 x11 ∧ _near_p_state e17 e3 x18)))

#check h₁ → h₂

end

Why am I getting the error below?

type expected
failed to synthesize instance
  CoeSort
    ((x e i : Type) →
      (e → x → Prop) →
        (x → Prop) →
          (x → Prop) →
            (x → Prop) →
              (e → x → Prop) →
                (e → x → i → Prop) →
                  (e → e → x → Prop) → (e → x → i → Prop) → (e → e → Prop) → (e → e → e → Prop) → Prop)
    ?m.1199

[Leonardo de Moura]

Note that h₁ is a function that returns Prop. In th following example f is not a constant, but a function.

variable (x : Nat)
def f := x + 1
#check f
example : f = fun x => x + 1 := rfl

[Alexandre Rademaker]

Sorry for the silly question, yes it makes sense.