proposition: Lemma noConfVec_eq_inv_eq {A n} (v v' : Vec A n) (e : NoConfusionHom_Vec _ _ v v') : noConfVec_eq _ _ (noConfVec_eq_inv _ _ e) = e.
proof: Proof. destruct v; revert e. depelim v'. simplify *; reflexivity. depelim v'. simplify *. simpl. reflexivity. Defined.
imports: Program Bvector List Relations Equations(Equations Signature DepElimDec) Utf8