proposition: Lemma matching_call3 : forall pat sub f lpat g lsub pb, o_list_size ((Term f lpat, Term g lsub):: pb) ((Term f (pat :: lpat), Term g (sub :: lsub)) :: pb).
proof: Proof. intros pat sub f lpat g lsub pb; unfold o_list_size; simpl. apply ->Nat.succ_lt_mono. rewrite <- Nat.add_assoc. pattern ((fix size_list (l : list term) : nat := match l with | nil => 0 | t :: lt => size t + size_list lt end) lpat + list_size (fun st : term * term => size (fst st)) pb); rewrite <- plus_O_n. apply Nat.add_lt_mono_r. unfold lt; apply size_ge_one; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)