proposition: Lemma oclause_neq_elim2 bc oc : oc \in (oclause_neq_elim bc) -> (oc.2 == [::]) && (oc.4 == bc.4).
proof: Proof. case: bc => bc1 bc2 bc3 bc4; elim: bc2 bc4 oc => [|t bc2 /= ih] bc4 /= oc. by rewrite inE; move/eqP; case: oc => ? ? ? oc4 /=; case=> _ /eqP -> _ /eqP. rewrite map_cat; move: (ih bc4 oc) => /= {ih}. elim: (neq_elim_aux bc3 bc2) => [| t2 l2 ih2] //= ih1. rewrite in_cons; case/orP. by move/eqP; case: oc {ih1 ih2} => ? ? ? ? [] /= _ -> _ ->; rewrite !eqxx. rewrite mem_cat; case/orP=> [hoc1|]. apply: ih2; first by move=> hoc2; apply: ih1; rewrite in_cons hoc2 orbT. by rewrite mem_cat hoc1. rewrite in_cons; case/orP=> [| hoc1]. by move/eqP; case: {ih1 ih2} oc=> ? ? ? ? [] /= _ -> _ ->; rewrite !eqxx. apply: ih2; first by move=> hoc2; apply: ih1; rewrite in_cons hoc2 orbT. by rewrite mem_cat hoc1 orbT. 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)