fact: Definition vec_fill {A: UU} (a: A): ∏ n: nat, vec A n := nat_rect (λ n: nat, vec A n) [()] (λ (n: nat) (v: vec A n), a ::: v).
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers