proposition: Lemma SameADTs_Trans: forall (av : Type) (m0 m1 m2 : StringMap.t (Value av)), SameADTs m0 m1 -> SameADTs m1 m2 -> SameADTs m0 m2.
proof: Proof. unfold SameADTs; t_Morphism. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid