proposition: Lemma projn_prod_of_vec : forall A n (xs : vector A n) i (hi : i<n), projn (prod_of_vec xs) hi = Vnth xs hi.
proof: Proof. intro A. induction xs; intros i hi. lia. simpl. destruct i as [|i]; fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)