proposition: Lemma canon_lim3 i n a lambda (Ha: T1nf a) (Hlambda: T1nf lambda) (Hlim :T1limit lambda) : canon (cons a n lambda) i = cons a n (canon lambda i).
proof: Proof. rewrite -g2h_eqE g2h_canon !g2h_cons canon_lim3. by rewrite -g2h_canon. 1,2 : by rewrite hnf_g2h. by rewrite T1limit_ref h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)