proposition: Lemma matching_call2 : forall pat sub f lpat g lsub pb, o_list_size ((pat,sub) :: nil) ((Term f (pat :: lpat), Term g (sub :: lsub)) :: pb).
proof: Proof. intros pat sub f lpat g lsub pb; unfold o_list_size; simpl. auto with arith. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)