proposition: Lemma SN_rel1_tail : forall n (v : vector A (S n)), SN (Vrel1 R) v -> SN (Vrel1 R) (Vtail v).
proof: Proof. induction 1. VSntac x. apply SN_intro. intros. ded (H0 (Vcons (Vhead x) y)). rewrite H1 in H3. apply H3. simpl. unfold Vhead_tail. simpl. apply right_sym. hyp. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)