proposition: Lemma nat_cast_eq_rect: forall (P : nat -> Type), forall (n m : nat) (e: n = m) (pn: P n), nat_cast P e pn = eq_rect n P pn m e.
proof: Proof. destruct e. revert dependent P; induction n; simpl; intros. - reflexivity. - rewrite IHn. reflexivity. Qed.