proposition: Lemma canon_lim1 i (lambda: T1) : T1nf lambda -> T1limit lambda -> canon (phi0 lambda) i = phi0 (canon lambda i).
proof: Proof. move => Hnf Hlim; rewrite /canon. have H: hcanon (T1.phi0 (g2h lambda)) i = T1.phi0 (hcanon (g2h lambda) i). { rewrite -Canon.canon_lim1 => //. - move: Hnf; by rewrite hnf_g2h. - by rewrite T1limit_ref h2g_g2hK. } by rewrite phi0_ref H. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)