proposition: Lemma eq_unitTypes_eq_types : forall M N, length (appUnits M) = length (appUnits N) -> (forall p Ma Na, nth_error (appUnits M) p = Some Ma -> nth_error (appUnits N) p = Some Na -> type Ma = type Na) -> type M = type N.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall N, length (appUnits M) = length (appUnits N) -> (forall p Ma Na, nth_error (appUnits M) p = Some Ma -> nth_error (appUnits N) p = Some Na -> type Ma = type Na ) -> type M = type N). apply subterm_wf. clear M; intros M IH N MNunits H. destruct (isApp_dec M) as [Mapp | Mnapp]. destruct (isApp_dec N) as [Napp | Nnapp]. assert (type (appBodyL Mapp) = type (appBodyL Napp)). apply IH. apply appBodyL_subterm. rewrite (appUnits_app M Mapp) in MNunits. rewrite (appUnits_app N Napp) in MNunits. rewrite !length_app in MNunits. simpl in MNunits; lia. intros; apply (H p Ma Na). rewrite (appUnits_app M Mapp). rewrite nth_app_left; trivial. apply nth_some with Ma; trivial. rewrite (appUnits_app N Napp). rewrite nth_app_left; trivial. apply nth_some with Na; trivial. term_inv M; term_inv N. absurd (length (appUnits M) = length (appUnits N)); trivial. rewrite (appUnits_app M Mapp). rewrite (appUnits_notApp N Nnapp). rewrite length_app; try_solve. term_inv (appBodyL Mapp). rewrite (appUnits_app Tr I). rewrite length_app; simpl; lia. destruct (isApp_dec N) as [Napp | Nnapp]. absurd (length (appUnits M) = length (appUnits N)); trivial. rewrite (appUnits_app N Napp). rewrite (appUnits_notApp M Mnapp). rewrite length_app; try_solve. term_inv (appBodyL Napp). rewrite (appUnits_app Tr I). rewrite length_app; simpl; lia. apply (H 0 M N). rewrite (appUnits_notApp M Mnapp); trivial. rewrite (appUnits_notApp N Nnapp); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)