>>128
レス大感謝です。さて、また私にとって難題です。エラーが出る最小限の
手順を用意しましたので、偉い方、どうかお付き合いください。
第1の例
Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A).

Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).

Theorem Eab : forall (a b:Set), ((a = b) \/ (b = a)) -> a = b.
Proof.
intros a b Hab.
assert (Hta:(a = b) /\ (b = a)).
apply Ee.
unfold Eqt.
assumption.(*ここでエラーが出ます*)
Qed.

これは、Display implicit argumentsとDeactivate notations display
をすることによって、Implicitな変数が原因であることがわかりました。