fact: Definition eval_rel : red_triple -> red_triple -> Prop := fun tr1 tr2 => let ectx1 := red_ctx tr1 in let ectx2 := red_ctx tr2 in let t1 := red_tm tr1 in let t2 := red_tm tr2 in TmEvalRel (ectx1, t1) (ectx2, t2).
imports: List Arith Bool