proposition: Lemma inputs_output : forall p T (h : p <= arity T), inputs (output T p) = Vsub (inputs T) (inputs_output_aux h).
proof: Proof. induction p; destruct T; simpl; intro h. refl. apply Vtail_eq. rewrite Vsub_cons, Vsub_id. refl. lia. assert (h' : p <= arity T2). lia. rewrite IHp with (h:=h'), Vsub_cons. apply Vsub_pi. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)