An Example Instantiation (Example.v)

This example demonstrates how to instantiate the module types of Sections 3 and 4.

Require Import Util.
Require Import Section3_Requirements.
Require Import Section3_Infrastructure.
Require Import Section3_Proofs.
Require Import Section4_Requirements.
Require Import Section4_Infrastructure.
Require Import Section4_Proofs.
Require Import Section5.
Require Import List.
Require Import Nat.
Require Import Coq.Arith.Arith.
Require Import Wf.
Require Import Wellfounded.Inverse_Image.
Require Import ProofIrrelevance.

Import Relation_Operators.
Import List.
Import ListNotations.

The Toy Language

Here, we define a simple nominal language. Literals are just class names drawn from CName with decidable equality cname_deq. For each class, there exists a finite list of superclasses. The inheritance relation created by superclasses is well-founded, which we express by requiring that there is a linearization that is maintained by the superclasses relation (super_lin).

Module Toy <: Traditional.

  Parameter CName : Type.
  Parameter cname_deq : forall cnl cnr : CName, {cnl = cnr} + {cnl <> cnr}.
  Parameter superclasses : CName -> list CName.
  Parameter linearization : CName -> nat.
  Parameter super_lin : forall sup sub : CName, In sup (superclasses sub) -> linearization sup < linearization sub.

  Definition Lit := CName.
  Notation T := (UIType Lit).

Declarative Subtyping

There are two literal subtyping rule schemata drule: Only the latter one has premises. Using <:: for the inheritance relation created by superclasses, the rules could be written as: 
              c <:: c'    c' <: c''
    ------    ---------------------
    c <: c          c <: c''

  Inductive drule : Lit -> Lit -> Type :=
  | drefl (cn : CName) : drule cn cn
  | dstep (cn cn' cn'' : CName) : In cn' (superclasses cn) -> drule cn cn''
  .

  Definition DRule : Lit -> Lit -> Type := drule.

  Inductive dpremise {l r : Lit} : DRule l r -> T -> T -> Prop :=
  | dprem_step (cn' : CName) (HInh : In cn' (superclasses l)) : dpremise (dstep l cn' r HInh) (TLit cn') (TLit r)
  .
  Arguments dpremise : clear implicits.

  Definition DPremise : forall {l r : Lit}, DRule l r -> T -> T -> Prop := dpremise.
  Notation dsub := (dsubf (@DPremise)).

Reductive Subtyping

In this language, the reductive literal subtyping rules are the same as the declarative literal subtyping rules. Note that this does not mean that the full reductive subtyping rules are the same as the declarative ones; the declarative ones add explicit reflexivity and transitivity rules.

  Inductive rrule : Lit -> Lit -> Type :=
  | rrefl (cn : CName) : rrule cn cn
  | rstep (cn cn' cn'' : CName) : In cn' (superclasses cn) -> rrule cn cn''
  .

  Definition RRule : Lit -> Lit -> Type := rrule.

  Inductive rpremise {l r : Lit} : RRule l r -> T -> T -> Prop :=
  | rprem_step (cn' : CName) (HInh : In cn' (superclasses l)) : rpremise (rstep l cn' r HInh) (TLit cn') (TLit r)
  .
  Arguments rpremise : clear implicits.

  Definition RPremise : forall {l r : Lit}, RRule l r -> T -> T -> Prop := rpremise.
  Notation rsub := (rsubf (@RPremise)).

Proofs of the Requirements of Section 3

Requirement 1: Syntax-Directedness

For every pair of literals ll and lr, the set of applicable rules RRule ll lr must be computable and finite (SyntaxDirectedness_Rules). For every rule r, the set of premises RPremise r must be computable and finite (SyntaxDirectedness_Premises).

  Lemma SyntaxDirectedness_Rules : forall ll lr : Lit, { rrules : list (RRule ll lr) | forall r : RRule ll lr, In r rrules }.
    intros ll lr. exists ((map_in (superclasses ll) (fun lsup => rstep ll lsup lr)) ++ (match cname_deq ll lr with left e => match e with eq_refl => rrefl ll end :: nil | right _ => nil end)). intro r. destruct r.
      apply in_app_iff. right. destruct (cname_deq cn cn).
        assert (Heq : e = eq_refl cn) by (apply proof_irrelevance). rewrite -> Heq. apply in_eq.
        destruct (n (eq_refl cn)).
      apply in_app_iff. left. unfold map_in. pose proof i as i'. generalize (incl_refl (superclasses cn)). revert i'. generalize (superclasses cn) at 1 2 5. intros l inl lsuper. induction l; destruct inl; subst; simpl.
        left. f_equal. apply proof_irrelevance.
        right. apply IHl. assumption.
  Qed.

  Lemma SyntaxDirectedness_Premises : forall {ll lr : Lit} (r : RRule ll lr), { rpremises : list (prod T T) | forall pl pr : T, RPremise r pl pr <-> In (pair pl pr) rpremises }.
    destruct r.
      exists []. intros tl tr; split; intros H; inversion H.
      exists [((TLit cn'), (TLit cn''))]. intros tl tr; split; intros H; inversion H; subst.
        apply in_eq.
        inversion H0; subst. constructor; fail.
        inversion H0.
  Qed.

Requirement 2: Well-Foundedness

There exists a function m from pairs of types to some set M with a well-founded (mltwf) relation mlt satisfying the following inequalities: m_ui_l, m_ui_r, and m_lit.
NOTE: for m_ui_l and m_ui_r, the paper technically only allows the reflexive closure of mlt, not the reflexive transitive closure. Again, this means that the requirement here is weaker than specified in the paper.

  Definition M : Type := nat.
  Definition mlt : M -> M -> Prop := lt.
  Definition mltwf : well_founded mlt := lt_wf.
  Fixpoint m (tl tr : T) : M :=
    match tl with
    | TLit l => linearization l
    | TTop => 0
    | TBot => 0
    | TUni tl' tr' => max (m tl' tr) (m tr' tr)
    | TIsect tl' tr' => max (m tl' tr) (m tr' tr)
    end.

  Lemma crtmlt_le : forall nl nr : nat, clos_refl_trans M mlt nl nr <-> le nl nr.
    intros nl nr; split; intros H.
      induction H.
        apply Nat.lt_le_incl. assumption.
        apply le_refl.
        apply le_trans with y; assumption.
      apply le_lt_or_eq in H. destruct H as [H | H]; [apply rt_step | subst; apply rt_refl]; assumption.
  Qed.

  Lemma m_ui_l : forall (tl tl' tr : T), subui tl tl' -> (clos_refl_trans M mlt) (m tl tr) (m tl' tr).
    intros tl tl' tr Hsub. inversion Hsub; subst; simpl; apply crtmlt_le; apply Nat.le_max_r || apply Nat.le_max_l.
  Qed.

  Lemma m_ui_r : forall (tl tr tr' : T), subui tr tr' -> (clos_refl_trans M mlt) (m tl tr) (m tl tr').
    intros tl tl' tr Hsub. apply crtmlt_le. induction tl; simpl; try reflexivity.
      apply Nat.max_le_compat; assumption.
      apply Nat.max_le_compat; assumption.
  Qed.
  Lemma m_lit : forall {ll lr : Lit} (r : RRule ll lr), forall pl pr : T, RPremise r pl pr -> mlt (m pl pr) (m (TLit ll) (TLit lr)).
    intros ll lr r tl tr Hprem. destruct r.
      inversion Hprem.
      inversion Hprem; subst; simpl. apply super_lin. assumption.
  Qed.

Requirement 3: Literal Reflexivity

For each literal l, there exists an RRule l l such that all premises have the same type on the left- and right-hand side.

  Lemma LiteralReflexivity : forall l : Lit, exists r : RRule l l, forall pl pr : T, RPremise r pl pr -> pl = pr.
    intros l. exists (rrefl l). intros tl tr Hprem. inversion Hprem.
  Qed.

Requirement 4: Reductive-to-Declarative Literal Conversion

Each reductive subtyping rule can be converted into a declarative subtyping proof where the premises of the reductive subtyping rule are assumed.

  Lemma RRuleToDProof : forall {ll lr : Lit} (r : RRule ll lr), dsuba (@DPremise) (RPremise r) (TLit ll) (TLit lr).
    intros ll lr r. induction r.
      apply dsuba_lit with (drefl cn); intros tl tr Hprem; inversion Hprem.
      apply dsuba_lit with (dstep cn cn' cn'' i); intros tl tr Hprem; inversion Hprem; subst. apply dsuba_assume. apply rprem_step.
  Qed.

Requirement 5: Declarative-to-Reductive Literal Conversion

Each declarative subtyping rule can be converted into a reductive subtyping proof where the premises of the reductive subtyping rule are assumed and monotonicity holds.
NOTE: this is a weaker requirement than in the paper as we allow monotonicity.

  Lemma DRuleToRProof : forall {ll lr : Lit} (r : DRule ll lr), rsubam (@RPremise) (DPremise r) (TLit ll) (TLit lr).
    intros ll lr r. induction r.
      apply ram_lit with (rrefl cn); intros tl tr Hprem; inversion Hprem.
      apply ram_lit with (rstep cn cn' cn'' i); intros tl tr Hprem; inversion Hprem; subst. apply ram_assumption. apply dprem_step.
  Qed.

Requirement 6: Literal Transitivity

For each pair of reductive literal rules rl rr that share a middle (right-hand in rl, left-hand in rr) literal lm, there exists a combined rule r between the left-hand literal of rl and the right-hand literal of rr, and each of the premises can be proven assuming local transitivity of the premises of rl and rr. Due to contravariance, it is possible that the premises of rl and rr might be composed in the opposite order.

   Lemma LiteralTransitivity : forall {ll lm lr : Lit} (rl : RRule ll lm) (rr : RRule lm lr),
     exists r : RRule ll lr,
       forall pl pr : T, RPremise r pl pr ->
          exists pm : T, (rsubam (@RPremise) (RPremise rl) pl pm /\ rsubam (@RPremise) (RPremise rr) pm pr) \/ (rsubam (@RPremise) (RPremise rr) pl pm /\ rsubam (@RPremise) (RPremise rl) pm pr).
    intros ll lm lr rl rr.
      destruct rl.
        exists rr. intros tl tr Hprem. inversion Hprem; subst. exists (TLit cn'). left. split.
          apply ram_lit with (rrefl cn'). intros tl tr Hprem'. inversion Hprem'.
          apply ram_assumption. assumption.
        destruct rr.
          exists (rstep cn cn' cn0 i). intros tl tr Hprem. inversion Hprem; subst. exists (TLit cn'). right. split.
            apply ram_lit with (rrefl cn'). intros tl tr Hprem'. inversion Hprem'.
            apply ram_assumption; assumption.
          exists (rstep cn cn' cn'' i). intros tl tr Hprem. inversion Hprem; subst. exists (TLit cn0). left. split.
            apply ram_assumption. constructor; fail.
            apply ram_lit with (rstep cn0 cn'0 cn'' i0). intros tl tr Hprem'. apply ram_assumption. assumption.
  Qed.

End Toy.

Extending the Toy Language: Object or Null

Here, we define a simple extension for our toy language: TTop is equivalent to Object ∪ Null. We define two special class names Object and Null that have linearization 0 and therefore cannot have superclasses. Null cannot have any subclasses Null_final, while everything that is not Null or Object must have superclasses. Therefore, every other class must effectively (transitively) extend Object.

Module ObjectOrNull <: (Intersector Toy).
  Import Toy.
  Module M_SopInfrastructure := SOP_Infrastructure Toy.
  Import M_SopInfrastructure.
  Import M_SopInfrastructure.M_TraditionalDec.
  Import M_SopInfrastructure.M_TraditionalDec.M_Infrastructure.

  Parameter Object : CName.
  Parameter Null : CName.
  Parameter Object_lin : linearization Object = 0.
  Parameter Null_lin : linearization Null = 0.
  Parameter Null_final : forall cn : CName, ~ In Null (superclasses cn).
  Parameter Lit_supers : forall cn : CName, cn = Object \/ cn = Null \/ (superclasses cn) <> [].

Basic Components

Our extension relation extension/ext (Coq does not like inductives to fill module parameter slots directly) simply declares that TTop should be a subtype of Object ∪ Null. The intersector intersect maps the empty list of literals (which corresponds to TTop) to that type and otherwise just returns the intersection of the given literals. The intersected predicate intersect holds for any non-empty list of literals (i.e. not TTop). The rest of the module proves Requirements 7 - 12, which means this module can be used to instantiate Integrated as follows: Integrated Toy ObjectOrNull. That module will then provide proofs that integrated subtyping using intersect provides a decidable subtyping relation for declarative subtyping with the additional axiom that TTop <: Object ∪ Null.

  Inductive ext : T -> T -> Prop :=
  | ext_objectornull : ext TTop (TUni (TLit Object) (TLit Null))
  .

  Definition extension : T -> T -> Prop := ext.
  Notation esub := (dsubda (@DPremise) extension).

  Definition intersect (ls : list Lit) : T :=
    match ls with
    | nil => (TUni (TLit Object) (TLit Null))
    | cons l ls' => Intersect (l :: ls')
    end.

  Definition intersected (ls : list Lit) : Prop := ls <> [].

Proofs of Requirements

Requirement 7: Intersector Completeness

The integrator Integrate intersect incorporates all the extensions in extension into traditional declarative subtyping.

  Lemma IntersectorCompleteness : forall tl tr : T, extension tl tr -> dsub (Integrate intersect tl) tr.
    intros tl tr Hext. destruct Hext. unfold Integrate. unfold intersect. simpl. apply dsuba_refl.
  Qed.

Requirement 8: Intersector Soundness

The intersector intersect integrates nothing more than what the extensions in extension can deduce via extended subtyping.

  Lemma IntersectorSoundness : forall ls : list Lit, esub (Intersect ls) (intersect ls).
    induction ls; simpl.
      apply dsubda_assume. constructor.
      apply dsubda_int_r.
        apply dsubda_int_ll.
        apply dsubda_int_lr.
  Qed.

Requirement 9: Measure Preservation

The integrator Integrate intersect preserves the termination measure. The paper technically only implies that the reflexive closure of mlt can be used here, so allowing the reflexive transitive closure here is a weaker requirement than in the paper.

  Lemma measure_lits : forall tl tr : T, (m tl tr) = fold_right max 0 (map (fun l => (m (TLit l) tr)) (lits tl)).
    intros tl. induction tl; intros tr; try reflexivity.
      simpl. rewrite -> IHtl1. rewrite -> IHtl2. clear IHtl1 IHtl2. induction (lits tl1); [reflexivity|]. simpl. rewrite <- Nat.max_assoc. rewrite <- IHl. reflexivity.
      simpl. rewrite -> IHtl1. rewrite -> IHtl2. clear IHtl1 IHtl2. induction (lits tl1); [reflexivity|]. simpl. rewrite <- Nat.max_assoc. rewrite <- IHl. reflexivity.
      simpl. symmetry. apply Nat.max_0_r.
  Qed.

  Lemma Integrate_lits {f : list Lit -> T}: forall lsx : list Lit, (forall ls : list Lit, incl (lits (f ls)) (ls ++ lsx)) -> forall t : T, incl (lits (Integrate f t)) ((lits t) ++ lsx).
    intros lxs Hf t. generalize dependent f. generalize dependent lxs. induction t; intros lxs f Hf.
      apply Hf.
      simpl. intros x HIn; inversion HIn.
      simpl; intros x HIn; apply in_app_or in HIn; destruct HIn as [HIn | HIn]; [apply (IHt1 lxs f) in HIn; [|assumption] | apply (IHt2 lxs f) in HIn; [|assumption]]; apply in_app_iff in HIn; (destruct HIn as [HIn | HIn]; apply in_app_iff; [left; apply in_app_iff | right; assumption]); [left | right]; assumption.
      simpl. rewrite <- app_assoc. apply IHt1. intros ls.
      assert (Hincl : forall l l1 l2 l3 : list Lit, incl l (l1 ++ (l2 ++ l3)) -> incl l (l2 ++ l1 ++ l3)) by (intros l l1 l2 l3 Hincl; intros x HIn; apply Hincl in HIn; apply in_app_iff in HIn; destruct HIn as [HIn | HIn]; [apply in_app_iff; right; apply in_app_iff; left; assumption|apply in_app_iff in HIn; destruct HIn as [HIn | HIn]; [apply in_app_iff; left; assumption|apply in_app_iff; right; apply in_app_iff; right; assumption]]). apply Hincl. apply IHt2. intros ls0. apply Hincl. rewrite -> app_assoc. apply Hf.
      simpl. apply Hf.
  Qed.

  Lemma integrate_incl : forall ls : list Lit, incl (lits (intersect ls)) (ls ++ [Object; Null]).
    intros ls. induction ls.
      apply incl_refl.
      simpl. intros x [HIn | HIn]; subst; [apply in_eq|]; apply in_cons; apply in_app_iff; left. clear IHls a. induction ls.
        inversion HIn.
        simpl in *. destruct HIn as [HIn | HIn]; subst; [left; reflexivity | right; apply IHls; assumption].
  Qed.

  Definition clt (cnl cnr : CName) : Prop := In cnl (superclasses cnr).
  Definition clt_lin (cnl cnr : CName) : Prop := linearization cnl < linearization cnr.

  Lemma acc_lin_acc_clt : forall cn : CName, Acc clt_lin cn -> Acc clt cn.
    intros cn Hacc. induction Hacc.
      constructor. intros cn Hclt. unfold clt in Hclt. apply super_lin in Hclt. apply H0 in Hclt. assumption.
  Qed.

  Lemma clt_lin_wf : well_founded clt_lin.
    apply (wf_inverse_image CName nat lt). apply lt_wf.
  Qed.

  Lemma clt_wf : well_founded clt.
    unfold well_founded. intros cn. apply acc_lin_acc_clt. apply clt_lin_wf.
  Qed.

  Lemma MeasurePreservation : forall tl tr : T, clos_refl_trans M mlt (m (Integrate intersect tl) tr) (m tl tr).
    intros tl tr. apply crtmlt_le. pose proof (Integrate_lits [Object; Null] integrate_incl tl). repeat rewrite -> measure_lits. apply le_trans with (fold_right max 0 (map (fun l : Lit => m (TLit l) tr) (lits tl ++ [Object; Null]))).
      remember (lits (Integrate intersect tl)) as ti. clear Heqti. remember (lits tl ++ [Object; Null]) as ta. clear Heqta. generalize dependent ti. clear tl. induction ta; intros tl Hincl.
        destruct tl.
          reflexivity.
          pose proof (Hincl l (in_eq l tl)) as Hn. inversion Hn.
        apply incl_max. intros x HIn. apply in_map_iff. apply in_map_iff in HIn. destruct HIn as [x' [Heq HIn]]. subst. exists x'. split; [reflexivity|]. apply Hincl. assumption.
      simpl. clear H. induction (lits tl).
        simpl. rewrite -> Object_lin. rewrite -> Null_lin. reflexivity.
        simpl. apply Nat.max_le_compat_l. assumption.
  Qed.

Requirement 10: Literal Dereliction

The intersector 'adds information' to a type, i.e. the result of applying the intersector to a list of literals is a traditional reductive subtype of the straightforward intersection of of those literals.

  Lemma LiteralDereliction : forall ls : list Lit, rsub (intersect ls) (Intersect ls).
    intros ls. destruct ls.
      repeat constructor; fail.
      apply rsub_refl.
  Qed.

Requirement 11: Intersector Integrated

The result of applying the intersector to a list of literals counts as Integrated using the provided intersected predicate.

  Lemma IntersectorIntegrated : forall ls : list Lit, Integrated intersected (intersect ls).
    intros ls. unfold intersect. induction ls; simpl.
      split; intros Hn; inversion Hn.
      apply ProductOfLiterals_Integrated_int; [apply Intersect_ProductOfLiterals|]. destruct ls.
        simpl. intros Hn; inversion Hn.
        revert IHls. apply Integrated_mono. intros ls0 HInt. intros Hn; inversion Hn.
  Qed.

Requirement 12: Literal Promotion

For every two lists of literals ls and ls', and list of reductive literal subtyping rules rs ⊆ RRule such that
Forall (fun l' : Lit => Exists (fun r : (sig2T RRule) => proj2T2 r = l') rs) ls' /\ incl (map proj2T1 rs)
if intersected ls holds then there exists a list of reductive literal subtyping rules rs' such that intersect ls' is of the form ... ∪ ⋂ (map proj2T2 rs') ∪ ... and for all reductive literal subtyping rules r' in rs':
In (proj2T1 r') ls /\ forall tl tr : T, RPremise (proj2V r') tl tr -> rsubam (@RPremise) (fun tl' tr' => Exists (fun r => RPremise (proj2V r) tl' tr') rs) tl tr) rs')

  Lemma Tlits_intersect : forall (ls : list Lit) (Hpol : ProductOfLiterals (Intersect ls)), Tlits (Intersect ls) Hpol = ls.
    intros ls Hpol. induction ls.
      reflexivity.
      simpl. f_equal. apply IHls.
  Qed.

  Lemma rsubam_object : forall l l' : Lit, In l (superclasses l') -> rsubam (@RPremise) (fun _ _ => False) (TLit l) (TLit Object).
    intros l l' Hsc. generalize dependent l'. generalize dependent l. apply (well_founded_ind clt_wf (fun l => forall l' : Lit, In l (superclasses l') -> rsubam (@RPremise) (fun _ _ => False) (TLit l) (TLit Object))). intros l IH l' HIn. pose proof (Lit_supers l) as [Hobj | [Hnull | Hsups]]; subst.
      apply rsub_rsubam. apply rsub_refl.
      apply Null_final in HIn. contradiction.
      destruct (superclasses l) eqn: Hl.
        contradiction Hsups; reflexivity.
        assert (HInc : In c (superclasses l)) by (rewrite -> Hl; apply in_eq). pose proof (IH _ HInc _ HInc). apply (@ram_lit Lit RRule (@RPremise) (fun _ _ => False) l Object (rstep l c Object HInc)). intros tl tr Hprem. inversion Hprem; subst. assumption.
  Qed.

  Lemma LiteralPromotion : forall (ls ls' : list Lit) (rs : list (sig2T RRule)), Forall (fun l' : Lit => Exists (fun r : (sig2T RRule) => proj2T2 r = l') rs) ls' -> incl (map proj2T1 rs) ls -> intersected ls -> exists rs' : list (sig2T RRule), Exists_Intersection (fun ls'' => ls'' = map proj2T2 rs' /\ incl (map proj2T1 rs') ls /\ Forall (fun r' : sig2T RRule => forall tl tr :T, RPremise (proj2V r') tl tr -> rsubam (@RPremise) (fun tl' tr' => Exists (fun r => RPremise (proj2V r) tl' tr') rs) tl tr) rs') (intersect ls').
    intros ls ls' rs Hfa Hincl Hint. destruct ls'.
      simpl. destruct ls; [contradiction Hint; reflexivity|]. pose proof (Lit_supers l) as [Hobj | [Hnull | Hsups]]; subst.
        exists [(exist2T Object Object (rrefl Object))]. left; split ; [reflexivity | split; simpl; [intros x HIn; inversion HIn; [|contradiction]; subst; apply in_eq|]]. constructor; [|constructor]. intros tl tr Hprem. inversion Hprem.
        exists [(exist2T Null Null (rrefl Null))]. right; split ; [reflexivity | split; simpl; [intros x HIn; inversion HIn; [|contradiction]; subst; apply in_eq|]]. constructor; [|constructor]. intros tl tr Hprem. inversion Hprem.
        destruct (superclasses l) as [|sc scs] eqn:Hsc.
          contradiction Hsups; reflexivity.
          assert (HIn : In sc (superclasses l)) by (rewrite -> Hsc; apply in_eq). exists [(exist2T l Object (rstep l sc Object HIn))]. left. split; [reflexivity | split; simpl; [intros x HInx; inversion HInx; [|contradiction]; subst; apply in_eq|]]. constructor; [|constructor]. intros tl tr Hprem. inversion Hprem; subst; simpl in *. apply rsubam_mono with (A := fun _ _ => False); [intros; contradiction|]. apply rsubam_object with l; assumption.
      unfold intersect. unfold Intersect. unfold fold_right. apply Forall_exists_project in Hfa. destruct Hfa as [rs' [Hincl' Hfa]]. exists rs'. apply Exists_Intersection_int_exists. fold (fold_right (fun l => TIsect (TLit l)) TTop (l :: ls')). fold (Intersect (l :: ls')). exists (Intersect_ProductOfLiterals (l :: ls')). split; [rewrite -> Tlits_intersect|split].
        inversion Hfa; subst. simpl. f_equal. clear Hfa. rename H3 into Hfa. induction Hfa; [reflexivity|]. simpl; subst; f_equal. apply IHHfa. intros x [HIn | HIn]; apply Hincl'; subst; [apply in_eq | apply in_cons; apply in_cons; assumption].
        intros x HIn. apply in_map_iff in HIn. destruct HIn as [r [Heq HIn]]. subst. apply Hincl' in HIn. apply Hincl. apply in_map_iff. exists r. split; [reflexivity | assumption].
        inversion Hfa; subst; simpl. constructor.
          intros tl tr Hprem. apply ram_assumption. apply Exists_exists. exists y. split; [apply Hincl'; apply in_eq | assumption].
          clear Hfa; rename H3 into Hfa; induction Hfa; constructor.
            intros tl tr Hprem. apply ram_assumption. apply Exists_exists. exists y0. split; [apply Hincl'; apply in_cons; apply in_eq | assumption].
            apply IHHfa. intros x' [HIn | HIn]; subst; apply Hincl'; [apply in_eq|]. apply in_cons; apply in_cons; assumption.
  Qed.

End ObjectOrNull.
This page has been generated by coqdoc