proposition: Lemma nat_rect3_ext {A B C D} (P := fun n => forall (a : A n) (b : B n a), C n a b -> D) (z z' : P 0) (Hz : forall a b c, z a b c = z' a b c) (s s' : forall n, P n -> P (S n)) (Hs : forall n f g (pf : forall a b c, f a b c = g a b c) a b c, s n f a b c = s' n g a b c) n a b c : nat_rect P z s n a b c = nat_rect P z' s' n a b c.
proof: Proof. revert a b c; induction n as [|n IHn]; simpl; intros. { apply Hz. } { apply Hs; intros. apply IHn. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.Morphisms Coq.ZArith.ZArith