proposition: Lemma matching_call1 : forall patt subj pb, o_list_size pb ((patt, subj) :: pb).
proof: Proof. intros patt sibj pb; unfold o_list_size; simpl. pattern (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)