+(* induction/inversion, abbastanza semplicemente, consiste nel generare i prod
+ * delle uguaglianze corrispondenti ai soli parametri destri appartenenti all'insieme S.
+ * Attenzione al caso base: cos'e` replace_lifting?
+ * S = {} e` il principio di induzione
+ * S = insieme_dei_destri e` il principio di inversione *)