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