proposition: Lemma Vforall_SN_rel1 : forall n (v : vector A n), Vforall (SN R) v -> SN (Vrel1 R) v.
proof: Proof. induction v; intros; apply SN_intro; intros. contr. simpl. eapply SN_inverse with (f := @Vhead_tail A n) (R := symprod R (Vrel1 R)). VSntac y. unfold Vhead_tail. simpl. simpl in H. destruct H. rewrite H1 in H0. inversion H0. apply SN_symprod. eapply SN_inv. apply H4. hyp. rewrite <- H7. apply IHv. hyp. apply SN_symprod. rewrite <- H6. hyp. eapply SN_inv. apply H4. apply IHv. hyp. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)