Description: Quantifier introduction when one pair of variables is distinct. Version of dveeq1 using ax-c11 . (Contributed by NM, 2-Jan-2002) (Proof modification is discouraged.) (New usage is discouraged.)