inductive Sets where| bool: Sets| ind: Nat -> Sets| fn: Sets -> Sets -> Setsdef Sets.denote: Sets -> Type| bool => Prop| ind => nat| fn i o => i.denote -> o.denotedef ifProp (p: Prop) (t: a) (e: a) : a := by  match Classical.lem p with  | Or.inl _ => t  | Or.inr _ => edef Model := Σ (s: Sets), s.denote