## § 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
```