qed.
theorem recursive3: ∀ x,y,z,t : nat.
C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? x) y) =
C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.
qed.
theorem recursive3: ∀ x,y,z,t : nat.
C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? x) y) =
C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.