proposition: Lemma pi_in_H : ~G pi.
proof: Proof. rewrite Gdef'; intro Dpi; inversion Dpi as [f l t [H1 H2]]; subst f. apply (proj2 (PPi t (Term pi l) H1 pi)). simpl; rewrite eq_symb_bool_refl; apply eq_refl. apply eq_refl. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)