P
roof_
T
erms_
T
erm_
R
ewriting
Proof_Term_Utils
Linear_Matching
Proof_Terms
Residual_Join_Deletion
Orthogonal_PT
Labels_and_Overlaps
Redex_Patterns