Clone defined logical symbols

Allow to substitute some already defined symbols, provided the definition are the same modulo the substitution. Works for logical function and predicates and for variant types (ADTs)

Fix #666 (closed)