proposition: Lemma tr_sn_beta_aeq : forall E v V, E |- v ~: V -> SN R_aeq v.
proof: Proof. set (I := fun (_ : So) => SN R_aeq). assert (cp_I : forall b, cp (I b)). intro b. apply cp_SN. apply tr_sn with (I:=I). hyp. intro f. set (n := arity (typ f)). apply int_arrow with (n:=n). refl. intros vs hvs. rewrite output_arity. simpl. set (b := output_base (typ f)). gen (cp_I b). intros [b1 b2 b3 b4]. cut (SN (clos_vaeq R) vs). 2:{ apply sn_clos_vaeq_intro. eapply vint_forall_sn. apply cp_I. apply hvs. } induction 1. apply b4. apply neutral_apps_fun. intros y r. destruct (R_aeq_apps_fun r) as [vs [h1 h2]]; clear r; subst. apply H0. hyp. rewrite <- h2. hyp. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(SN VecUtil LogicUtil SetUtil)