proposition: Lemma cast_same: forall (B: type) (t: interp_type B), cast B t = t.
proof: Proof. intros. unfold cast. pose proof (cast_impl_same B t) as P. apply proj1 in P. exact P. Qed.
imports: Arith Lia List FunctionalExtensionality