proposition: Lemma canon_succ i a (Ha: T1nf a): canon (T1succ a) i = a.
proof: Proof. rewrite -g2h_eqE g2h_canon g2h_succ Canon.canon_succ ?hnf_g2h => //. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)