proposition: Lemma tr_sn_SystemT : forall E v V, E |- v ~: V -> SN R_aeq v.
proof: Proof. apply tr_sn_beta_eta_rewrite_aeq. intros l r h; inversion h; subst; unfold lhs_fun, lhs_args, lhs_nb_args; simpl. eapply cc_arg' with (i:=1); refl. set (ls := [App FSucc n; u; v]). assert (hn : cc gt1 (Rec A) ls ST.empty n TNat). eapply cc_acc' with (g:=Succ) (us:=[n]) (i:=0); simpl; try refl. eapply cc_arg' with (i:=0); refl. assert (hv : cc gt1 (Rec A) ls ST.empty v (TNat ~~> A ~~> A)). eapply cc_arg' with (i:=2); simpl; refl. assert (hu : cc gt1 (Rec A) ls ST.empty u A). eapply cc_arg' with (i:=1); simpl; refl. eapply cc_app. eapply cc_app. apply hv. hyp. eapply cc_call' with (g:=Rec A) (us:=[n; u; v]); try refl. simpl. lia. unfold gt1, Def.gt_call, Rof, transp. apply right_lex. unfold Def.gt_args_lex, Rof, lexv; simpl. apply lex1. apply opt_intro. unfold gt. apply clos_aeq_intro_refl. apply t_step. eapply stacc_intro' with (i:=0) (f:=Succ) (ts:=[n]); try refl. intros i i1 i2. destruct i. simpl. hyp. destruct i. simpl. hyp. destruct i. simpl. hyp. lia. Unshelve. simpl; lia. simpl; lia. apply Acc_Succ. simpl; lia. simpl; lia. simpl; lia. simpl; lia. simpl; lia. simpl; lia. apply Acc_Succ. Qed.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec) CoLoR(VecUtil) CoLoR(LCompRewrite) CoLoR(SN LCall) CoLoR(EqUtil) CoLoR(LCompInt) CoLoR(LCompClos) CoLoR(Lexico)