proposition: Lemma g2h_plusE (a b: T1) : g2h (a + b) = T1.T1add (g2h a) (g2h b).
proof: Proof. apply symmetry, refines2_R, plus_ref. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)