proposition: Lemma proj_cons_fun_aux2 : forall f n m (Emn : n + m = arity f) v v1 v2, (forall i (Hi : i < n), red proj_cons # (Vnth v1 Hi) (Vnth v2 Hi)) -> red proj_cons # (Fun f (Vcast (Vapp v1 v) Emn)) (Fun f (Vcast (Vapp v2 v) Emn)).
proof: Proof. intro f. induction n; intros m Emn v v1 v2 Hin. rewrite (VO_eq v1), (VO_eq v2). simpl. apply rt_refl. assert (H0 : n < S n + m). lia. assert (H1 : m = S n + m - S n). lia. rewrite (Veq_app_cons (Vapp v1 v) H0), (Veq_app_cons (Vapp v2 v) H0). assert (Ve1 : forall x, Vsub (Vapp x v) (Veq_app_cons_aux2 H0) = (Vcast v H1)). intro x; pattern v at 2. rewrite <- (Vsub_app_r x v (Nat.le_refl (S n + m))), Vcast_sub. apply Vsub_pi. assert (Ve2 : forall x, Vsub (Vapp x v) (Veq_app_cons_aux1 H0) = (Vsub x (Veq_app_aux1 (Nat.le_succ_diag_r n)))). intro x. apply Veq_nth; intros. rewrite !Vnth_sub, Vnth_app. case (le_gt_dec (S n) (0 + i)); intro. lia. apply Vnth_eq; auto. rewrite (Ve1 v1), (Ve1 v2), (Ve2 v1), (Ve2 v2), !Vnth_app, !Vcast_cast. case (le_gt_dec (S n) n); intro H2. lia. set (v' := Vcast v H1); set (x := Vnth v1 H2); set (y := Vnth v2 H2). set (v1' := Vsub v1 (Veq_app_aux1 (Nat.le_succ_diag_r n))). set (v2' := Vsub v2 (Veq_app_aux1 (Nat.le_succ_diag_r n))). set (H3 := trans_eq (Veq_app_cons_aux3 H0) Emn). apply rt_trans with (y := Fun f (Vcast (Vapp v2' (Vcons x v')) H3)). apply IHn. intros. unfold v1', v2'. rewrite !Vnth_sub. apply Hin. apply proj_cons_fun_aux1. apply Hin. Qed.
imports: CoLoR(ATrs VecUtil ListUtil LogicUtil NatUtil RelUtil)