Library hydras.MoreAck.BadSubst

From hydras Require Import fol folProp folProof Languages folLogic primRec.
From Coq Require Import Arith.

Import FolNotations.

#[local] Arguments Ensembles.In {_} .
#[local] Arguments Ensembles.Add {_} .
#[local] Arguments atomic _ _ _ : clear implicits.
#[local] Arguments apply _ _ _ : clear implicits.

Module BadSubst.

  Fixpoint substF L (F : Formula L) v (t: Term L) :=
    match F with
  | equal t1 t2 ⇒ equal (substT t1 v t) (substT t2 v t)
  | atomic r s ⇒ atomic L r (substTs s v t)
  | impH G H ⇒ impH (substF L G v t) (substF L H v t)
  | notH G ⇒ notH (substF L G v t)
  | forallH w G ⇒ if Nat.eq_dec w v then F else forallH w (substF L G v t)
  end.

End BadSubst.

From Coq Require Import List.
Import ListNotations.

Module BadSubstF2.


End BadSubstF2.

From hydras Require Import FolExamples.
Import Toy.

Section BadExample.

  Let F := (allH 1, exH 2, v#1 ≠ f v#2)%fol.
  Let F1: Formula L := (exH 2, v#1 ≠ f v#2)%fol.


End BadExample.