proposition: Lemma Forall_make : forall n v P, P v -> Forall P (make n v).
proof: Proof. Proof using. introv N. induction n as [|n']. { rewrite make_zero. applys* Forall_nil. } { rewrite make_succ. applys* Forall_cons. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)