proposition: Lemma nat_cast_proof_irrel: forall (P : nat -> Type), forall (n m : nat) (e1 e2: n = m) (pn: P n), nat_cast P e1 pn = nat_cast P e2 pn.
proof: Proof. destruct e1. revert dependent P; induction n; simpl; intros. - reflexivity. - erewrite IHn. reflexivity. Qed.