theorem Cedar.Thm.ofRecordType_as_map (rty : List (Spec.Attr × Validation.QualifiedType)) : SymCC.TermType.ofRecordType rty = List.map (fun (x : Spec.Attr × Validation.QualifiedType) => match x with | (a, qty) => (a, SymCC.TermType.ofQualifiedType qty)) rty

Rephrases ofRecordType with map