proposition: Lemma canon_limit_strong lambda : T1nf lambda -> T1limit lambda -> forall b, T1nf b -> T1lt b lambda -> {i : nat | b < canon lambda i}.
proof: Proof. rewrite -(h2g_g2hK lambda) -nf_ref -T1limit_ref => Hnf Hlim b Hb. rewrite -(h2g_g2hK b) => Hblt; apply hlt_iff in Hblt. case (@canon_limit_strong (g2h lambda) Hnf Hlim (g2h b)). - split => //; rewrite hnf_g2h => //. - move => x Hx; exists x; rewrite -(h2g_g2hK b). rewrite -g2h_canon in Hx; rewrite !h2g_g2hK. move: Hx; rewrite -T1lt_iff => //. rewrite /canon -nf_ref; change (T1.nf (hcanon (g2h lambda) x)); apply nf_canon => //. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)