proposition: Lemma Tlt_Tle_compat_afs : Trel_compat Tlt_afs Tle_afs.
proof: Proof. intros t1 t2 t3; apply (Tlt_Tle_compat (afs t1) (afs t2) (afs t3)). Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)