proposition: Theorem eq_rect_nat_double : forall T (a b c : nat) x ab bc, eq_rect b T (eq_rect a T x b ab) c bc = eq_rect a T x c (eq_trans ab bc).
proof: Proof. intros. destruct ab. destruct bc. rewrite (UIP_dec eq_nat_dec (eq_trans eq_refl eq_refl) eq_refl). simpl. auto. Qed.
imports: Coq.Arith.Peano_dec Coq.Logic.Eqdep Coq.Logic.Eqdep_dec Coq.Program.Equality