§ 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