proposition: Lemma canonS_phi0_succE (i : nat) (gamma : T1): T1nf gamma -> canon (phi0 (T1succ gamma)) i.+1 = cons gamma i zero.
proof: Proof. rewrite -(h2g_g2hK gamma) /canon succ_ref phi0_ref g2h_h2gK => Hnf. change zero with (h2g T1.zero); rewrite Canon.canonS_phi0_succ_eqn ?h2g_cons =>//. - move: Hnf; rewrite h2g_g2hK; by rewrite /T1.nf nf_ref h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)