|
let rec réécrit_le = function G1_EE (G1_EE (e, e'), e'') -> réécrit_le (G1_EE (e, G1_EE (e', e''))) | G1_EE (G1_gEd e, e') -> G2_gEdE (réécrit_le e, réécrit_le e') | G1_EE (G1_0, e) -> réécrit_le e | G1_gEd e -> G2_gEdE (réécrit_le e, G2_0) | G1_0 -> G2_0;; let réécrit (G1_S e) = G2_S (réécrit_le e);; |