proposition: Lemma exp_consCE1 (x := \F 2) (a := zero) (n := 0)(b := T1omega): x ^(cons a n b) != x ^(cons a n zero) * x ^b.
proof: Proof. done. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)