proposition: Lemma tr_sn_beta_eta_rewrite_aeq : forall E v V, E |- v ~: V -> SN R_aeq v.
proof: Proof. eapply tr_sn_cc. apply I_cp. apply not_neutral_apps_fun. apply comp_acc. apply comp_fun. apply not_neutral_apps_fun. apply gt2_wf. apply gt2_mcaeq. apply gt2_gt1. apply gt2_clos_vaeq. apply lhs_cc_rhs. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)