proposition: Lemma T1nf_canon a i : T1nf a -> T1nf (canon a i).
proof: Proof. rewrite /canon -nf_ref => ?; apply nf_canon; by rewrite hnf_g2h. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)