Library LangAlg.terms_graphs

Using the translation of terms into primed weak terms we can reduce the axiomatic containment of 𝐓-terms to the ordering of graphs.

Set Implicit Arguments.

Require Import terms_w_terms w_terms_graphs.

Definition 𝕲t {X} (u : 𝐓 X) := 𝕲w π{𝐓_to_𝐖' u}.

Theorem 𝐓_inf_is_weak_graph_inf {X : Set} `{decidable_set X}:
   u v : 𝐓 X, u v 𝕲t u 𝕲t v.