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