proposition: Lemma canon_lim2 i n (lambda : T1) (Hnf: T1nf lambda) (Hlim: T1limit lambda): canon (cons lambda n.+1 zero) i = cons lambda n (phi0 (canon lambda i)).
proof: Proof. rewrite -g2h_eqE g2h_canon !g2h_cons canon_lim2. - congr T1.cons. - by rewrite -g2h_canon. - by rewrite hnf_g2h. - by rewrite T1limit_ref h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)