proposition: Lemma terms_of_neq_elim oc1 oc2: oc2 \in (oclause_neq_elim oc1) -> {subset (terms_of_oclause oc2) <= (terms_of_oclause oc1) ++ (map Opp oc1.2)}.
proof: Proof. case: oc1 => eq1 neq1 lt1 leq1 /=. elim: neq1 lt1 oc2 => [|t1 neq1 ih] lt1 [eq2 neq2 lt2 leq2] /=. by rewrite inE; case/eqP=> -> -> -> ->; rewrite !cats0 !cat0s. rewrite map_cat /= mem_cat -!map_comp; set f := fun _ => _. rewrite -/f in ih; case/orP. case/mapP=> y yin ye. move: (ih lt1 (f y)); rewrite mem_map //; last first. by move=> u v; rewrite /f /=; case. move/(_ yin); move: ye; rewrite /f /=; case=> -> -> -> -> /= h. move=> u. rewrite !mem_cat !in_cons orbAC orbC mem_cat -!orbA. case/orP; first by move->; rewrite !orbT. rewrite !orbA [_ || (_ \in eq1)]orbC; move: (h u); rewrite !mem_cat=> hu. by move/hu; do 2!(case/orP; last by move->; rewrite !orbT); move->. case/mapP=> y yin ye. move: (ih lt1 (f y)); rewrite mem_map //; last first. by move=> u v; rewrite /f /=; case. move/(_ yin); move: ye; rewrite /f /=; case=> -> -> -> -> /= h. move=> u; rewrite !mem_cat !in_cons orbAC orbC mem_cat -!orbA. case/orP; first by move->; rewrite !orbT. rewrite !orbA [_ || (_ \in eq1)]orbC; move: (h u); rewrite !mem_cat=> hu. by move/hu; do 2!(case/orP; last by move->; rewrite !orbT); move->. 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)