proposition: Lemma L_spec0 (f:nat -> nat) : L_spec zero f <-> forall k, f k.+1 = k.+1.
proof: Proof. rewrite /L_spec; split => H. move => k; inversion H => //. by left. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder) hydras(T1 E0) hydras(L_alpha) gaia_hydras(T1Bridge GCanon GPaths GHprime)