proposition: Lemma lam_aeq_l : forall t x u, Lam x u ~~ t -> exists y v, t = Lam y v /\ v ~~ rename x y u /\ (x = y \/ ~In y (fv u)).
proof: Proof. intros t x u h. apply lam_aeq_r. sym. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)