§ Embedding HOL in Lean

inductive Sets where
| bool: Sets
| ind: Nat -> Sets
| fn: Sets -> Sets -> Sets

def Sets.denote: Sets -> Type
| bool => Prop
| ind => nat
| fn i o => i.denote -> o.denote

def ifProp (p: Prop) (t: a) (e: a) : a := by
  match Classical.lem p with
  | Or.inl _ => t
  | Or.inr _ => e

def Model := Σ (s: Sets), s.denote