(*CSC: dovrebbe diventare da sinistra verso destra: *)
(*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H *)
(*CSC: per la roba che proviene da Coq questo non serve! *)
(*CSC: dovrebbe diventare da sinistra verso destra: *)
(*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H *)
(*CSC: per la roba che proviene da Coq questo non serve! *)