A simple LFC-style interactive proof assistant, written with a view towards studying proof modularity.