proposition: Lemma canon0_phi0_succE a: T1nf a -> canon (phi0 (T1succ a)) 0 = zero.
proof: Proof. rewrite -(h2g_g2hK a) -nf_ref /canon => Hnf. rewrite succ_ref phi0_ref g2h_h2gK Canon.canon0_phi0_succ_eqn => //. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)