proposition: Lemma SN_rel1_forall : forall n (v : vector A n), SN (Vrel1 R) v -> Vforall (SN R) v.
proof: Proof. induction v; intros; simpl. exact I. split. apply (SN_rel1_head H). apply IHv. apply (SN_rel1_tail H). Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)