proposition: Lemma cast_impl_same: forall (B: type) (t: interp_type B), fst (cast_impl B B) t = t /\ snd (cast_impl B B) t = t.
proof: Proof. induction B; intros; simpl; unfold id. - auto. - do 2 rewrite type_eqb_same. destruct (cast_impl B1 B1) as [fw1 bw1] eqn: E1. destruct (cast_impl B2 B2) as [fw2 bw2] eqn: E2. simpl in *. split; extensionality arg. + specialize (IHB1 arg). apply proj2 in IHB1. rewrite IHB1. specialize (IHB2 (t arg)). apply proj1 in IHB2. exact IHB2. + specialize (IHB1 arg). apply proj1 in IHB1. rewrite IHB1. specialize (IHB2 (t arg)). apply proj2 in IHB2. exact IHB2. Qed.
imports: Arith Lia List FunctionalExtensionality