proposition: Lemma oclause_leq_elim4 bc oc : oc \in (oclause_leq_elim bc) -> oc.4 == [::].
proof: Proof. case: bc => bc1 bc2 bc3 bc4; elim: bc4 bc1 bc3 oc => [|t bc4 ih] bc1 bc3 /= oc. by rewrite inE; move/eqP; case: oc => ? ? ? oc4 /=; case=> _ _ _ /eqP. rewrite map_cat; move: (ih bc1 bc3 oc) => /= {ih}. elim: (leq_elim_aux bc1 bc3 bc4) => [| t2 l2 ih2] //= ih1. rewrite in_cons; case/orP. by move/eqP; case: oc {ih1 ih2} => ? ? ? ? [] /= _ _ _ /eqP. 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=> ? ? ? ? [] /= _ _ _ /eqP. 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)