+ | expr2 NEQT expr2
+ { let dom1,mk_expr1 = $1 in
+ let dom2,mk_expr2 = $3 in
+ let dom3,mk_expr3 = mk_implicit () in
+ let dom = union dom1 (union dom2 dom3) in
+ dom, function interp ->
+ Cic.Appl [
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con",[]);
+ Cic.Appl
+ [Cic.MutInd
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
+ (mk_expr3 interp) ;
+ (mk_expr1 interp) ;
+ (mk_expr2 interp)
+ ]]
+ }