proposition: Lemma output_output : forall p q T, output (output T p) q = output T (p+q).
proof: Proof. induction p; destruct T; simpl; try refl. destruct q; refl. rewrite IHp. refl. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)