fact: Fixpoint subtract ts1 ts2 xs : option (seq term) := match ts1 with Expr n :: tsx1 => if has (exp n) ts2 then subtract tsx1 (efree n ts2) xs else subtract tsx1 ts2 (Expr n :: xs) | [::] => if ts2 is [::] then Some xs else None end.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)