proposition: Lemma proj_cons_fun_aux1 : forall f n m (Emn : n + S m = arity f) v1 v2 x y, red proj_cons # x y -> red proj_cons # (Fun f (Vcast (Vapp v1 (Vcons x v2)) Emn)) (Fun f (Vcast (Vapp v1 (Vcons y v2)) Emn)).
proof: Proof. intros f m n. induction 1. 2: apply rt_refl. apply rt_step. destruct H as [l H]; destruct H as [r H]; destruct H as [c H]. destruct H as [s H]. exists l. exists r. exists (Cont _ Emn v1 c v2). exists s. split. destruct H; auto. simpl. destruct H as [_ H]. destruct H as [H3 H4]. rewrite <- H3, <- H4. auto. apply rt_trans with (y := Fun f (Vcast (Vapp v1 (Vcons y v2)) Emn)); auto. Qed.
imports: CoLoR(ATrs VecUtil ListUtil LogicUtil NatUtil RelUtil)