proposition: Lemma phiE x : phi x = phi_rec phi x.
proof: Proof. have aux: forall n x, (size x < n)%N -> phia n x = (phi x). clear x; move => n; elim: n {1 3 4} n (leqnn n); first by case. move => k0 Hrec [] // k1; rewrite ltnS => k1k0. case => // a b c n d; rewrite ltnS => e3. move /and5P:(size_prop1 a b c n d) => [pa pb pc pd pe]. have la:= (leq_trans pa e3). have lb:= (leq_trans pb e3). have lc:= (leq_trans pc e3). have ld:= (leq_trans pd e3). have le: (size (cons a b c 0 d) <= k0)%N. by move:(leq_trans e3 k1k0). rewrite /phi /phia -/phia /phi_rec -/phi -/(phi_rec _ d). case dz: (d==zero). case n; first by rewrite /phi_rec_psi !Hrec //. by move => m; congr (phi1 _ _);rewrite /phi_rec_psi !Hrec. by congr phi1; rewrite !Hrec. case x => // a b c n d. move: (size_prop1 a b c n d). move/and5P=> [pa pb pc pd pe]. rewrite /phi /phia -/phia /phi_rec -/phi -/(phi_rec _ d). case dz: (d==zero). case n; first by rewrite /phi_rec_psi !aux. by move => m; congr (phi1 _ _);rewrite /phi_rec_psi !aux. by congr phi1; rewrite aux. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)