proposition: Lemma tr_sn_cc : forall E v V, E |- v ~: V -> SN R_aeq v.
proof: Proof. apply tr_sn with (I:=I). hyp. cut (forall c, SN gt2 c -> vint I (inputs (typ (call_fun c))) (call_args c) -> int I (output (typ (call_fun c)) (arity (typ (call_fun c)))) (apps (Fun (call_fun c)) (call_args c))). intros h f. apply int_arrow with (n:=arity(typ f)). refl. intros vs hvs. apply (h (mk_max_call f vs)). apply WF_inverse. apply gt2_wf. hyp. induction 1; clear H. destruct x as [[f n ts] e]; simpl; simpl in e. subst n. intro hts. rewrite output_arity. set (b := output_base (typ f)). gen (I_cp b); intros [b1 b2 b3 b4]. apply comp_fun. hyp. intros t' h. destruct (beta_eta_rewrite_aeq_apps_fun h) as [[vs [j1 j2]] |[m [ls [r [s [q [vs [h1 [h2 [h3 h4]]]]]]]]]]; clear h. subst t'. rewrite int_base, <- output_arity. apply (H0 (mk_max_call f vs)). apply gt2_clos_vaeq. hyp. hyp. simpl. rewrite <- j2. hyp. rewrite h4; clear h4. rewrite h3, vint_cast_term in hts. gen (lhs_cc_rhs h2). rewrite lhs_fun_eq, lhs_args_eq, cc_cast, lhs_nb_args_eq. intro hc. rewrite int_base. eapply int_apps. gen (vint_app_term_elim_r hts); intro hvs. apply hvs. assert (hm : 0 + m <= arity (typ f)). lia. eapply cc_comp with (ts:=ts) (gt1:=gt1) (gt2:=gt2) (ls:=ls) (h:=hm) (E:=XMap.empty); auto. rewrite h3, vint_cast_term. hyp. intros g us h. apply (H0 _ h). sym. gen (Vforall2_sub hm h3). rewrite Vsub_cast, Vsub_app_l. auto. lia. rewrite <- output_arity. setoid_rewrite <- h1 at 3. rewrite arrow_output. hyp. intros z T. rewrite empty_mapsto_iff. fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)