proposition: Lemma interp_tApp: forall e t1 t2 A B (f: interp_type A -> interp_type B) (a: interp_type A), interp_term e t1 = existT _ (tpArr A B) f -> interp_term e t2 = existT _ A a -> interp_term e (tApp t1 t2) = existT _ B (f a).
proof: Proof. intros. simpl. destruct (interp_term e t1) eqn: E1. destruct (interp_term e t2) eqn: E2. pose proof (EqdepFacts.eq_sigT_fst H). subst x. apply Eqdep_dec.inj_pair2_eq_dec in H. 2: apply type_eq_dec. subst i. pose proof (EqdepFacts.eq_sigT_fst H0). subst x0. apply Eqdep_dec.inj_pair2_eq_dec in H0. 2: apply type_eq_dec. subst i0. rewrite cast_same. reflexivity. Qed.
imports: Arith Lia List FunctionalExtensionality