Lean4
/-- A recursion principle for pairs of ZFA lists and proper ZFA prelists. -/
def inductionMut (C : Lists α → Sort*) (D : Lists' α true → Sort*) (C0 : ∀ a, C (atom a)) (C1 : ∀ l, D l → C (of' l))
(D0 : D Lists'.nil) (D1 : ∀ a l, C a → D l → D (Lists'.cons a l)) : PProd (∀ l, C l) (∀ l, D l) :=
by
suffices
∀ {b} (l : Lists' α b),
PProd (C ⟨_, l⟩)
(match b, l with
| true, l => D l
| false, _ => PUnit)
by exact ⟨fun ⟨b, l⟩ => (this _).1, fun l => (this l).2⟩
intro b l
induction l with
| atom => exact ⟨C0 _, ⟨⟩⟩
| nil => exact ⟨C1 _ D0, D0⟩
| cons' a l IH₁ IH =>
have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
exact ⟨C1 _ this, this⟩
