varias tatics of propositional logic

I return to coq art again, and found following tactics of propositional logic
intro(s) : reduce Env,Cxt-A-> B to Env,(A:Ctx) - B
apply H : reduce Env,(A->B:Ctx)-B to Env,(A->B:Ctx)-A
assumption : reduce Env,(A:Ctx) -A to Env,(A:Ctx) - true