proposition: Lemma liftUnOpCons n op b (p: BITS n) : liftUnOp op (consB b p) = consB (op b) (liftUnOp op p).
proof: Proof. by apply: eq_from_tnth=> i; rewrite !(tnth_nth (op b)). Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations