proposition: Lemma phiE_1 a b c n: phi (cons a b c n.+1 zero) = phi1 (cons a b c n zero) (phi [a, b, c]).
proof: Proof. by rewrite phiE /=; congr phi1; rewrite phiE /phi_rec eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)