proposition: Lemma fmerge_aux_ext f1 f2 g1 g2 i j : f1 =1 f2 -> g1 =1 g2 -> fmerge_aux f1 g1 i j =1 fmerge_aux f2 g2 i j.
proof: Proof. move=> fE gE n; elim: n i j => /= [i1 j1|n IH i j]; first by rewrite fE gE. by rewrite !(fE, gE, IH). Qed.
imports: mathcomp(all_ssreflect finmap)