<div dir="ltr">Dear,<div>I would like a theorem prover where I can add new tactics for proving properties of equational programs. I don't know if I can do it with metis, and if metis supports second order substitutions,<br clear="all"><div>many thanks,</div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">Moussa Demba<br><br><br></div></div></div></div>
</div></div>

<br>
<font face="Courier New" size="3">

</font><p align="center" style="margin:0cm 0cm 0pt;text-align:center;line-height:normal"><u>_{<span lang="AR-SA" style="color:red;font-size:12pt" dir="RTL"><font face="" size="2">بيان إخلاء المسؤولية</font></span>}</u><u>_{<span lang="AR-SA" style="color:red" dir="RTL"><br><font face="" size="2"></font></span>}</u></p><font face="" size="2">

</font><p align="center" style="margin:0cm 0cm 6pt;text-align:center;line-height:normal">_{<span lang="AR-SA" style="color:gray;font-size:10pt" dir="RTL"><font face="" size="2">إن المعلومات الواردة في هذا البريد الإلكتروني وأي ملفات مرفقة هي
معلومات خاصة بالمرسل إليه أو المتعامل و قد تحتوي على معلومات سرية أو مواد محمية
ولذلك يحظر على أي شخص آخر الإطلاع على محتويات هذا البريد الإلكتروني. الرجاء إذا
لم تكن أحد المعنيين باستلام هذا البريد الإلكتروني، المبادرة بإشعار المرسل فوراً
وحذف المواد التي يتضمنها البريد الإلكتروني. يمنع منعاً باتاً نسخ أو توزيع أو
اتخاذ أو إلغاء أي أجراء بالإعتماد على هذا البريد الإلكتروني. لا تتحمل
جامعة الجوف أي مسؤولية قانونية عن أي أضرار ناتجة عن أي فيروس أو برامج ترسل
بواسطة هذا البريد الإلكتروني .</font></span>}</p><font face="Courier New" size="3">

</font>