proposition: Lemma canonS_ocons_succE i n (gamma: T1)(Hnf : T1nf gamma) : canon (cons (T1succ gamma) n.+1 zero) i.+1 = cons (T1succ gamma) n (cons gamma i zero).
proof: Proof. rewrite -g2h_eqE g2h_canon !g2h_cons g2h_succ g2h_zero. by rewrite canonS_cons_succ_eqn2 ?hnf_g2h. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)