proposition: Lemma terms_of_leq_elim oc1 oc2: oc2 \in (oclause_leq_elim oc1) -> (terms_of_oclause oc2) =i (terms_of_oclause oc1).
proof: Proof. case: oc1 => eq1 neq1 lt1 leq1 /=. elim: leq1 eq1 lt1 oc2 => [|t1 leq1 ih] eq1 lt1 [eq2 neq2 lt2 leq2] /=. by rewrite inE; case/eqP=> -> -> -> -> ?. rewrite map_cat /= mem_cat -!map_comp; set f := fun _ => _. rewrite -/f in ih; case/orP. case/mapP=> [[y1 y2]] yin ye. move: (ih eq1 lt1 (f (y1, y2))); rewrite mem_map //; last first. by move=> [u1 u2] [v1 v2]; rewrite /f /=; case=> -> ->. move/(_ yin); move: ye; rewrite /f /=; case=> -> -> -> -> /= h. move=> u; rewrite in_cons (h u) !mem_cat in_cons. by rewrite orbC !orbA; set x := _ || (u \in lt1); rewrite orbAC. case/mapP=> [[y1 y2]] yin ye. move: (ih eq1 lt1 (f (y1, y2))); rewrite mem_map //; last first. by move=> [u1 u2] [v1 v2]; rewrite /f /=; case=> -> ->. move/(_ yin); move: ye; rewrite /f /=; case=> -> -> -> -> /= h u. rewrite !mem_cat !in_cons orbA orbCA -!orbA; move: (h u); rewrite !mem_cat=> ->. by rewrite orbC !orbA; set x := _ || (u \in lt1); rewrite orbAC. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)